/*  Novelties: A visual novel programming language based on JavaFX
    Copyright (C) 2008  Hao Xu

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
 * /
/*
 * Substitution.fx
 *
 * Created on Apr 13, 2008, 4:00:00 PM
 */

package avgengine.pred;

import java.util.Map;
import java.util.HashMap;
/**
 * @author ertri
 */

class Substitution  {
    attribute map : Map;
    operation subLiteral(l:Literal):Literal;
    operation subTerm(t:Term):Term;
    operation subTerms(t:Term*):Term*;
    operation subLiterals(t:Literal*):Literal*;
    operation subSub(t:Substitution):Substitution;
    
    operation add(v:Variable, t:Term);
    operation put(v:Variable, t:Term);
}

attribute Substitution.map = new HashMap();

operation Substitution.subLiteral(l) {
    return Literal{
        sign:l.sign
        p:l.p
        params:this.subTerms(l.params)
    };
}
operation Substitution.subLiterals(t:Literal*):Literal* {
    if(sizeof t == 0) {
        return t;
    }else {
        var t1 = t[n|indexof n > 0];
        var subst = subLiterals(t1);
        insert subLiteral(t[0]) as first into subst;
        
        
        return subst;
        
    }
}


operation Substitution.add(v,t) {
    var sub = Substitution{};
    var s = Substitution{};
    s.map.put(v.n,t);
    if(not map.isEmpty()){
        println("map.keySet() = {map.keySet()}");
        var itr = map.keySet().iterator();
        while(itr.hasNext()) {
            var ent = itr.next();
            sub.map.put(ent, s.subTerm((Term)map.get(ent)));
        }
    }
    this.map.clear();
    this.map.putAll(s.map);
    this.map.putAll(sub.map);
    println("map = {this.map}");
}
operation Substitution.put(v,t) {
    map.put(v.n,t);
}
operation Substitution.subTerm(l) {
    if(l instanceof Variable) {
        var t = (Term)this.map.get(((Variable)l).n);
        return if t == null then l else t;
    } else {
        return FunctionTerm {
            f:((FunctionTerm)l).f
            params:this.subTerms(((FunctionTerm)l).params)
        };
    }
}
operation Substitution.subTerms(l) {
    if(sizeof l == 0) {
        return l;} else {
        var subtl = subTerms(l[n|indexof n > 0]);
        insert subTerm(l[0]) as first into subtl;
        
        return subtl;
        }
}
operation Substitution.subSub(t) {
    var s = new Substitution{};
    var itr = t.map.keySet().iterator();
    s.map.putAll(this.map);
    while(itr.hasNext()) {
        var key = (String)itr.next();
        s.put(Variable{n:key}, subTerm((Term)t.map.get(key)));
    }

    return s;
    //;;;//;;;//;;;;//;//;//;
}